package Services;

import Impl.Dir;

public interface MoteurJeuService {
	// INVARIANTS 
	// inv: getPasRestants()>=0
	
	// CONSTRUCTEURS
	// pre: init(i) require i>0 && TerrainService::isStarted(terrain)
	// post: haveHeroMove()==false
	// post: haveObjectMove()==false
	// post: getPasRestants()==i
	// post: getTerrain()==terrain
	// post: estFinie()==false         
	// post: estGagne()==false 
	public void init(int i, TerrainService terrain);
	
	// OBSERVATEURS
	public boolean estFinie();
	public boolean estGagne();
	public TerrainService getTerrain();
	public int getPasRestants();
	public boolean haveObjectMove();
	public boolean haveHeroMove();
	
	// OPERATEURS
	// pre: verif() require !estFinie() && haveHeroMove() && haveObjectMove()
	// post: getPasRestants()==getPasRestants()@pre
	// post: haveHeroMove()==false
	// post: haveObjectMove()==false
	// post:
	//		if(TerrainService::getNbDiamant(getTerrain()@pre)==0)
	//			getTerrain()==TerrainService::openDoor(getTerrain()@pre)
	//		else getTerrain()==getTerrain()@pre
	// post:         
	//              int x = TerrainService::getXJoueur(getTerrain()@pre)         
	//              int y = TerrainService::getYJoueur(getTerrain()@pre)        
	//              Type type=TerrainService::getTypeBloc(getTerrain()@pre, x, y)                  
	//              if(TerrainService::getOldTypeBloc(getTerrain()@pre, x, y)==Type.SortieOuverte)         
	//                      estFinie()==true         
	//                      estGagne()==true         
	//              else if(type==Type.Diamant || type==Type.Rocher || getPasRestants()@pre==0)         
	//                      estFinie()==true         
	//                      estGagne()==false         
	//              else          
	//                      estFinie()==estFinie()@pre         
	//                      estGagne()==estGagne()@pre 
	public void verif();
	
	// pre: moveObjects() require !estFinie() && haveHeroMove() && !haveObjectMove() 
	// post: haveHeroMove()==haveHeroMove()@pre
	// post: haveObjectMove()==true
	// post: getPasRestants()==getPasRestants()@pre
	// post: estFinie()==estFinie()@pre         
	// post: estGagne()==estGagne()@pre 
	// post:
	//		TerrainService tmp = getTerrain()
	//		forall y in [TerrainService::getSizeY(getTerrain()), 1] and x in [TerrainService::getSizeY(getTerrain()), 1] 
	//			if(TerrainService::getTypeBloc(getTerrain(), x, y) in {Type.Rocher, Type.Diamant})
	//					if(!TerrainService::isChanged(getTerrain(),x, y) && (TerrainService::getTypeBloc(getTerrain(),x, y+1) in {Type.Vide, Type.Hero}))
	//						tmp==TerrainService::moveObject(tmp, x, y, x, y+1)
	//
	//  	getTerrain()==TerrainService::validate(tmp)
	public void moveObjects();
	
	// pre: moveHero(d) require !estFinie() &&!haveObjectMove() && !haveHeroMove() 
	// post: haveHeroMove()==true
	// post: haveObjectMove()==haveObjectMove()@pre
	// post: getPasRestants()==getPasRestants()@pre-1
	// post: estFinie()==estFinie()@pre         
	// post: estGagne()==estGagne()@pre 
	// post:
	//		entier x = TerrainService::getXJoueur(getTerrain())
	//		entier y = TerrainService::getYJoueur(getTerrain())
	//		if (d==Dir.Haut){
	//			Type type = TerrainService::getTypeBloc(getTerrain()@pre,x, y-1)
	//			if(type C {Vide,Terre,SortieOuverte})
	//				getTerrain()==TerrainService::putHero(getTerrain()@pre, x, y-1)
	//			else
	//				getTerrain()==getTerrain()@pre
	//		}
	//		else if (d==Dir.Bas){
	//			Type type = TerrainService::getTypeBloc(getTerrain(), x, y+1)
	//			if(type C {Vide,Terre,SortieOuverte,Diamant})
	//				getTerrain()==TerrainService::putHero(getTerrain()@pre, x, y+1)
	//			else
	//				getTerrain()==getTerrain()@pre
	//		}
	//		else if (d==Dir.Droite){
	//			Type type = TerrainService::getTypeBloc(getTerrain()@pre,x+1, y)
	//			if(type C {Vide,Terre,SortieOuverte,Diamant})
	//				getTerrain()==TerrainService::putHero(getTerrain()@pre, x+1, y)
	//			else if(type==Rocher &&  TerrainService::getTypeBloc(x+2, y)==Type.Vide)
	//				getTerrain()==TerrainService::putHero(TerrainService::moveObject(getTerrain()@pre,x+1,y,x+2,y), x+1, y)
	//			else
	//				getTerrain()==getTerrain()@pre
	//		}
	//		else if (d==Dir.Gauche){
	//			Type type = TerrainService::getTypeBloc(getTerrain()@pre,x-1, y)
	//			if(type C {Vide,Terre,SortieOuverte,Diamant})
	//				getTerrain()==TerrainService::putHero(getTerrain()@pre, x-1, y)
	//			else if(type==Rocher &&  TerrainService::getTypeBloc(x-2, y)==Vide)
	//				getTerrain()==TerrainService::putHero(TerrainService::moveObject(getTerrain()@pre,x-1,y,x-2,y), x-1, y)
	//			else
	//				getTerrain()==getTerrain()@pre
	//		}
	//		else {
	//			getTerrain()==getTerrain()@pre
	//		}
	public void moveHero(Dir d);
}
